-
Notifications
You must be signed in to change notification settings - Fork 54
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add format stdin smoke tests #2019
Conversation
@@ -8,7 +8,7 @@ axiom trace : {A : Type} → A → A; | |||
|
|||
terminating | |||
f : Nat → Nat → Nat; | |||
f x y := if (x == 0) y (trace x >>> (f (sub x 1) y)); | |||
f x y := if (x == 0) y (trace x >>> f (sub x 1) y); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just curiosity, did you change this manually? or it was the formatter?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That is after make pre-commit
command work, not sure how it was not caught earlier
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Exactly. pre-commit locally runs the Juvix formatter and the CI as well. I'm supprised, a new mystery to my stack.
65d7803
to
4ca27d5
Compare
Is this ready to review or is it a draft? I just rebased it because the CI failed to build the project. |
@jonaprieto ye, this PR only adds tests. I am working on what we discussed today, which is handling the command without filepath but with stdin better. Regarding failing tests, locally, my tests are passing. It seem to be different behaviour possibly due to the Linux machine run? Not sure that this is the only reason for failure |
As figured out, I somehow used the older version of the Can confirm, that currently the Also, I wonder what the priority should be if you specify both |
👍
Based on the usage case, that is the vscode extension, I'd keep giving priority to --stdin input. |
juvix format
command #2008As I were trying to fix the behaviour of
format
command with the--stdin
global option, I noticed that actually it is already behaves the same was asdev scope
command (which was the desire at least at this point).So, no actual behaviour of the command is channged, only a few tests added to showcase some edge cases of the command with the
--stdin
option together.Here are the highlights:
dev scope
andformat
even if withstdin
the content of the file comes from the input.format
command expects the stdin input to be a proper moduleI think that some of the above behaviours we can consider to change. Let me know what do you think about any of that.
Otherwise, the
dev scope
command can be replaced withformat
.